H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.307 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral b => b -> [a] -> ([a],[a])

genericSplitAt

0 xs

([],xs)

genericSplitAt

_ []

([],[])

genericSplitAt

n (x : xs)

n > 0

(x : xs',xs'')

where

vv9

genericSplitAt (n - 1) xs

xs'

(\(xs',_) ->xs') vv9

xs''

(\(_,xs'') ->xs'') vv9

genericSplitAt

_ _

error []

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(xs',_)→xs'

is transformed to

xs'0 (xs',_) = xs'

The following Lambda expression

\(_,xs'')→xs''

is transformed to

xs''0 (_,xs'') = xs''

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral b => b -> [a] -> ([a],[a])

genericSplitAt

0 xs

([],xs)

genericSplitAt

_ []

([],[])

genericSplitAt

n (x : xs)

n > 0

(x : xs',xs'')

where

vv9

genericSplitAt (n - 1) xs

xs'

xs'0 vv9

xs''

xs''0 vv9

xs''0

(_,xs'')

xs''

xs'0

(xs',_)

xs'

genericSplitAt

_ _

error []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case compare x y of
EQ → o

LT → LT

GT → GT

is transformed to

primCompAux0 o EQ = o

primCompAux0 o LT = LT

primCompAux0 o GT = GT

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral b => b -> [a] -> ([a],[a])

genericSplitAt

0 xs

([],xs)

genericSplitAt

_ []

([],[])

genericSplitAt

n (x : xs)

n > 0

(x : xs',xs'')

where

vv9

genericSplitAt (n - 1) xs

xs'

xs'0 vv9

xs''

xs''0 vv9

xs''0

(_,xs'')

xs''

xs'0

(xs',_)

xs'

genericSplitAt

_ _

error []

module Maybe where

import qualified List
import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral b => b -> [a] -> ([a],[a])

genericSplitAt

0 xs

([],xs)

genericSplitAt

_ []

([],[])

genericSplitAt

n (x : xs)

n > 0

(x : xs',xs'')

where

vv9

genericSplitAt (n - 1) xs

xs'

xs'0 vv9

xs''

xs''0 vv9

xs''0

(_,xs'')

xs''

xs'0

(xs',_)

xs'

genericSplitAt

_ _

error []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral b => b -> [a] -> ([a],[a])

genericSplitAt

0 xs

([],xs)

genericSplitAt

vw []

([],[])

genericSplitAt

n (x : xs)

n > 0

(x : xs',xs'')

where

vv9

genericSplitAt (n - 1) xs

xs'

xs'0 vv9

xs''

xs''0 vv9

xs''0

(vx,xs'')

xs''

xs'0

(xs',vy)

xs'

genericSplitAt

vz wu

error []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

genericSplitAt 0 xs = ([],xs)

genericSplitAt vw [] = ([],[])

genericSplitAt n (x : xs)

| n > 0

= (x : xs',xs'')

where

vv9 = genericSplitAt (n - 1) xs

xs' = xs'0 vv9

xs'' = xs''0 vv9

xs''0 (vx,xs'') = xs''

xs'0 (xs',vy) = xs'

genericSplitAt vz wu = error []

is transformed to

genericSplitAt vvx xs = genericSplitAt5 vvx xs

genericSplitAt vw [] = genericSplitAt3 vw []

genericSplitAt n (x : xs) = genericSplitAt2 n (x : xs)

genericSplitAt vz wu = genericSplitAt0 vz wu

genericSplitAt0 vz wu = error []

genericSplitAt2 n (x : xs) =

genericSplitAt1 n x xs (n > 0)

where

genericSplitAt1 n x xs True = (x : xs',xs'')

genericSplitAt1 n x xs False = genericSplitAt0 n (x : xs)

vv9 = genericSplitAt (n - 1) xs

xs' = xs'0 vv9

xs'' = xs''0 vv9

xs''0 (vx,xs'') = xs''

xs'0 (xs',vy) = xs'

genericSplitAt2 vuy vuz = genericSplitAt0 vuy vuz

genericSplitAt3 vw [] = ([],[])

genericSplitAt3 vvv vvw = genericSplitAt2 vvv vvw

genericSplitAt4 True vvx xs = ([],xs)

genericSplitAt4 vvy vvz vwu = genericSplitAt3 vvz vwu

genericSplitAt5 vvx xs = genericSplitAt4 (vvx == 0) vvx xs

genericSplitAt5 vwv vww = genericSplitAt3 vwv vww

The following Function with conditions

compare x y

| x == y

= EQ

| x <= y

= LT

| otherwise

= GT

is transformed to

compare x y = compare3 x y

compare0 x y True = GT

compare2 x y True = EQ

compare2 x y False = compare1 x y (x <= y)

compare1 x y True = LT

compare1 x y False = compare0 x y otherwise

compare3 x y = compare2 x y (x == y)

The following Function with conditions

gcd' x 0 = x

gcd' x y = gcd' y (x `rem` y)

is transformed to

gcd' x vwx = gcd'2 x vwx

gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vwx = x

gcd'1 vwy vwz vxu = gcd'0 vwz vxu

gcd'2 x vwx = gcd'1 (vwx == 0) x vwx

gcd'2 vxv vxw = gcd'0 vxv vxw

The following Function with conditions

gcd 0 0 = error []

gcd x y =

gcd' (abs x) (abs y)

where

gcd' x 0 = x

gcd' x y = gcd' y (x `rem` y)

is transformed to

gcd vxx vxy = gcd3 vxx vxy

gcd x y = gcd0 x y

gcd0 x y =

gcd' (abs x) (abs y)

where

gcd' x vwx = gcd'2 x vwx

gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vwx = x

gcd'1 vwy vwz vxu = gcd'0 vwz vxu

gcd'2 x vwx = gcd'1 (vwx == 0) x vwx

gcd'2 vxv vxw = gcd'0 vxv vxw

gcd1 True vxx vxy = error []

gcd1 vxz vyu vyv = gcd0 vyu vyv

gcd2 True vxx vxy = gcd1 (vxy == 0) vxx vxy

gcd2 vyw vyx vyy = gcd0 vyx vyy

gcd3 vxx vxy = gcd2 (vxx == 0) vxx vxy

gcd3 vyz vzu = gcd0 vyz vzu

The following Function with conditions

reduce x y

| y == 0

= error []

| otherwise

= x `quot` d :% (y `quot` d)

where

d = gcd x y

is transformed to

reduce x y = reduce2 x y

reduce2 x y =

reduce1 x y (y == 0)

where

d = gcd x y

reduce0 x y True = x `quot` d :% (y `quot` d)

reduce1 x y True = error []

reduce1 x y False = reduce0 x y otherwise

The following Function with conditions

absReal x

| x >= 0

= x

| otherwise

= `negate` x

is transformed to

absReal x = absReal2 x

absReal1 x True = x

absReal1 x False = absReal0 x otherwise

absReal0 x True = `negate` x

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ LetRed

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral a => a -> [b] -> ([b],[b])

genericSplitAt	vvx xs	=	genericSplitAt5 vvx xs
genericSplitAt	vw []	=	genericSplitAt3 vw []
genericSplitAt	n (x : xs)	=	genericSplitAt2 n (x : xs)
genericSplitAt	vz wu	=	genericSplitAt0 vz wu

genericSplitAt0

vz wu

error []

genericSplitAt2

n (x : xs)

genericSplitAt1 n x xs (n > 0)

where

genericSplitAt1	n x xs True	=	(x : xs',xs'')
genericSplitAt1	n x xs False	=	genericSplitAt0 n (x : xs)

vv9

genericSplitAt (n - 1) xs

xs'

xs'0 vv9

xs''

xs''0 vv9

xs''0

(vx,xs'')

xs''

xs'0

(xs',vy)

xs'

genericSplitAt2

vuy vuz

genericSplitAt0 vuy vuz

genericSplitAt3	vw []	=	([],[])
genericSplitAt3	vvv vvw	=	genericSplitAt2 vvv vvw

genericSplitAt4	True vvx xs	=	([],xs)
genericSplitAt4	vvy vvz vwu	=	genericSplitAt3 vvz vwu

genericSplitAt5	vvx xs	=	genericSplitAt4 (vvx == 0) vvx xs
genericSplitAt5	vwv vww	=	genericSplitAt3 vwv vww

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

genericSplitAt1 n x xs (n > 0)

where

genericSplitAt1 n x xs True = (x : xs',xs'')

genericSplitAt1 n x xs False = genericSplitAt0 n (x : xs)

vv9 = genericSplitAt (n - 1) xs

xs' = xs'0 vv9

xs'' = xs''0 vv9

xs''0 (vx,xs'') = xs''

xs'0 (xs',vy) = xs'

are unpacked to the following functions on top level

genericSplitAt2Xs'0 vzv vzw (xs',vy) = xs'

genericSplitAt2GenericSplitAt1 vzv vzw n x xs True = (x : genericSplitAt2Xs' vzv vzw,genericSplitAt2Xs'' vzv vzw)

genericSplitAt2GenericSplitAt1 vzv vzw n x xs False = genericSplitAt0 n (x : xs)

genericSplitAt2Xs'' vzv vzw = genericSplitAt2Xs''0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Vv9 vzv vzw = genericSplitAt (vzv - 1) vzw

genericSplitAt2Xs' vzv vzw = genericSplitAt2Xs'0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Xs''0 vzv vzw (vx,xs'') = xs''

The bindings of the following Let/Where expression

reduce1 x y (y == 0)

where

d = gcd x y

reduce0 x y True = x `quot` d :% (y `quot` d)

reduce1 x y True = error []

reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level

reduce2Reduce0 vzx vzy x y True = x `quot` reduce2D vzx vzy :% (y `quot` reduce2D vzx vzy)

reduce2Reduce1 vzx vzy x y True = error []

reduce2Reduce1 vzx vzy x y False = reduce2Reduce0 vzx vzy x y otherwise

reduce2D vzx vzy = gcd vzx vzy

The bindings of the following Let/Where expression

gcd' (abs x) (abs y)

where

gcd' x vwx = gcd'2 x vwx

gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vwx = x

gcd'1 vwy vwz vxu = gcd'0 vwz vxu

gcd'2 x vwx = gcd'1 (vwx == 0) x vwx

gcd'2 vxv vxw = gcd'0 vxv vxw

are unpacked to the following functions on top level

gcd0Gcd' x vwx = gcd0Gcd'2 x vwx

gcd0Gcd' x y = gcd0Gcd'0 x y

gcd0Gcd'2 x vwx = gcd0Gcd'1 (vwx == 0) x vwx

gcd0Gcd'2 vxv vxw = gcd0Gcd'0 vxv vxw

gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd'1 True x vwx = x

gcd0Gcd'1 vwy vwz vxu = gcd0Gcd'0 vwz vxu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ LetRed

                        ↳ HASKELL

                          ↳ NumRed

mainModule List

((genericSplitAt :: Int -> [a] -> ([a],[a])) :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral a => a -> [b] -> ([b],[b])

genericSplitAt	vvx xs	=	genericSplitAt5 vvx xs
genericSplitAt	vw []	=	genericSplitAt3 vw []
genericSplitAt	n (x : xs)	=	genericSplitAt2 n (x : xs)
genericSplitAt	vz wu	=	genericSplitAt0 vz wu

genericSplitAt0

vz wu

error []

genericSplitAt2	n (x : xs)	=	genericSplitAt2GenericSplitAt1 n xs n x xs (n > 0)
genericSplitAt2	vuy vuz	=	genericSplitAt0 vuy vuz

genericSplitAt2GenericSplitAt1	vzv vzw n x xs True	=	(x : genericSplitAt2Xs' vzv vzw,genericSplitAt2Xs'' vzv vzw)
genericSplitAt2GenericSplitAt1	vzv vzw n x xs False	=	genericSplitAt0 n (x : xs)

genericSplitAt2Vv9

vzv vzw

genericSplitAt (vzv - 1) vzw

genericSplitAt2Xs'

vzv vzw

genericSplitAt2Xs'0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Xs''

vzv vzw

genericSplitAt2Xs''0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Xs''0

vzv vzw (vx,xs'')

xs''

genericSplitAt2Xs'0

vzv vzw (xs',vy)

xs'

genericSplitAt3	vw []	=	([],[])
genericSplitAt3	vvv vvw	=	genericSplitAt2 vvv vvw

genericSplitAt4	True vvx xs	=	([],xs)
genericSplitAt4	vvy vvz vwu	=	genericSplitAt3 vvz vwu

genericSplitAt5	vvx xs	=	genericSplitAt4 (vvx == 0) vvx xs
genericSplitAt5	vwv vww	=	genericSplitAt3 vwv vww

module Maybe where

import qualified List
import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ LetRed

                        ↳ HASKELL

                          ↳ NumRed

                            ↳ HASKELL

                              ↳ Narrow

mainModule List

(genericSplitAt :: Int -> [a] -> ([a],[a]))

module List where

import qualified Maybe
import qualified Prelude

genericSplitAt :: Integral a => a -> [b] -> ([b],[b])

genericSplitAt	vvx xs	=	genericSplitAt5 vvx xs
genericSplitAt	vw []	=	genericSplitAt3 vw []
genericSplitAt	n (x : xs)	=	genericSplitAt2 n (x : xs)
genericSplitAt	vz wu	=	genericSplitAt0 vz wu

genericSplitAt0

vz wu

error []

genericSplitAt2	n (x : xs)	=	genericSplitAt2GenericSplitAt1 n xs n x xs (n > fromInt (Pos Zero))
genericSplitAt2	vuy vuz	=	genericSplitAt0 vuy vuz

genericSplitAt2GenericSplitAt1	vzv vzw n x xs True	=	(x : genericSplitAt2Xs' vzv vzw,genericSplitAt2Xs'' vzv vzw)
genericSplitAt2GenericSplitAt1	vzv vzw n x xs False	=	genericSplitAt0 n (x : xs)

genericSplitAt2Vv9

vzv vzw

genericSplitAt (vzv - fromInt (Pos (Succ Zero))) vzw

genericSplitAt2Xs'

vzv vzw

genericSplitAt2Xs'0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Xs''

vzv vzw

genericSplitAt2Xs''0 vzv vzw (genericSplitAt2Vv9 vzv vzw)

genericSplitAt2Xs''0

vzv vzw (vx,xs'')

xs''

genericSplitAt2Xs'0

vzv vzw (xs',vy)

xs'

genericSplitAt3	vw []	=	([],[])
genericSplitAt3	vvv vvw	=	genericSplitAt2 vvv vvw

genericSplitAt4	True vvx xs	=	([],xs)
genericSplitAt4	vvy vvz vwu	=	genericSplitAt3 vvz vwu

genericSplitAt5	vvx xs	=	genericSplitAt4 (vvx == fromInt (Pos Zero)) vvx xs
genericSplitAt5	vwv vww	=	genericSplitAt3 vwv vww

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="genericSplitAt",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="genericSplitAt vzz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="genericSplitAt vzz3 vzz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="genericSplitAt5 vzz3 vzz4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="genericSplitAt4 (vzz3 == fromInt (Pos Zero)) vzz3 vzz4",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="genericSplitAt4 (primEqInt vzz3 (fromInt (Pos Zero))) vzz3 vzz4",fontsize=16,color="burlywood",shape="box"];78[label="vzz3/Pos vzz30",fontsize=10,color="white",style="solid",shape="box"];7 -> 78[label="",style="solid", color="burlywood", weight=9];
78 -> 8[label="",style="solid", color="burlywood", weight=3];
79[label="vzz3/Neg vzz30",fontsize=10,color="white",style="solid",shape="box"];7 -> 79[label="",style="solid", color="burlywood", weight=9];
79 -> 9[label="",style="solid", color="burlywood", weight=3];
8[label="genericSplitAt4 (primEqInt (Pos vzz30) (fromInt (Pos Zero))) (Pos vzz30) vzz4",fontsize=16,color="burlywood",shape="box"];80[label="vzz30/Succ vzz300",fontsize=10,color="white",style="solid",shape="box"];8 -> 80[label="",style="solid", color="burlywood", weight=9];
80 -> 10[label="",style="solid", color="burlywood", weight=3];
81[label="vzz30/Zero",fontsize=10,color="white",style="solid",shape="box"];8 -> 81[label="",style="solid", color="burlywood", weight=9];
81 -> 11[label="",style="solid", color="burlywood", weight=3];
9[label="genericSplitAt4 (primEqInt (Neg vzz30) (fromInt (Pos Zero))) (Neg vzz30) vzz4",fontsize=16,color="burlywood",shape="box"];82[label="vzz30/Succ vzz300",fontsize=10,color="white",style="solid",shape="box"];9 -> 82[label="",style="solid", color="burlywood", weight=9];
82 -> 12[label="",style="solid", color="burlywood", weight=3];
83[label="vzz30/Zero",fontsize=10,color="white",style="solid",shape="box"];9 -> 83[label="",style="solid", color="burlywood", weight=9];
83 -> 13[label="",style="solid", color="burlywood", weight=3];
10[label="genericSplitAt4 (primEqInt (Pos (Succ vzz300)) (fromInt (Pos Zero))) (Pos (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];10 -> 14[label="",style="solid", color="black", weight=3];
11[label="genericSplitAt4 (primEqInt (Pos Zero) (fromInt (Pos Zero))) (Pos Zero) vzz4",fontsize=16,color="black",shape="box"];11 -> 15[label="",style="solid", color="black", weight=3];
12[label="genericSplitAt4 (primEqInt (Neg (Succ vzz300)) (fromInt (Pos Zero))) (Neg (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];12 -> 16[label="",style="solid", color="black", weight=3];
13[label="genericSplitAt4 (primEqInt (Neg Zero) (fromInt (Pos Zero))) (Neg Zero) vzz4",fontsize=16,color="black",shape="box"];13 -> 17[label="",style="solid", color="black", weight=3];
14[label="genericSplitAt4 (primEqInt (Pos (Succ vzz300)) (Pos Zero)) (Pos (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="genericSplitAt4 (primEqInt (Pos Zero) (Pos Zero)) (Pos Zero) vzz4",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="genericSplitAt4 (primEqInt (Neg (Succ vzz300)) (Pos Zero)) (Neg (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="genericSplitAt4 (primEqInt (Neg Zero) (Pos Zero)) (Neg Zero) vzz4",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="genericSplitAt4 False (Pos (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="genericSplitAt4 True (Pos Zero) vzz4",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="genericSplitAt4 False (Neg (Succ vzz300)) vzz4",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="genericSplitAt4 True (Neg Zero) vzz4",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="genericSplitAt3 (Pos (Succ vzz300)) vzz4",fontsize=16,color="burlywood",shape="box"];84[label="vzz4/vzz40 : vzz41",fontsize=10,color="white",style="solid",shape="box"];22 -> 84[label="",style="solid", color="burlywood", weight=9];
84 -> 26[label="",style="solid", color="burlywood", weight=3];
85[label="vzz4/[]",fontsize=10,color="white",style="solid",shape="box"];22 -> 85[label="",style="solid", color="burlywood", weight=9];
85 -> 27[label="",style="solid", color="burlywood", weight=3];
23[label="([],vzz4)",fontsize=16,color="green",shape="box"];24[label="genericSplitAt3 (Neg (Succ vzz300)) vzz4",fontsize=16,color="burlywood",shape="box"];86[label="vzz4/vzz40 : vzz41",fontsize=10,color="white",style="solid",shape="box"];24 -> 86[label="",style="solid", color="burlywood", weight=9];
86 -> 28[label="",style="solid", color="burlywood", weight=3];
87[label="vzz4/[]",fontsize=10,color="white",style="solid",shape="box"];24 -> 87[label="",style="solid", color="burlywood", weight=9];
87 -> 29[label="",style="solid", color="burlywood", weight=3];
25[label="([],vzz4)",fontsize=16,color="green",shape="box"];26[label="genericSplitAt3 (Pos (Succ vzz300)) (vzz40 : vzz41)",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="genericSplitAt3 (Pos (Succ vzz300)) []",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="genericSplitAt3 (Neg (Succ vzz300)) (vzz40 : vzz41)",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="genericSplitAt3 (Neg (Succ vzz300)) []",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="genericSplitAt2 (Pos (Succ vzz300)) (vzz40 : vzz41)",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="([],[])",fontsize=16,color="green",shape="box"];32[label="genericSplitAt2 (Neg (Succ vzz300)) (vzz40 : vzz41)",fontsize=16,color="black",shape="box"];32 -> 35[label="",style="solid", color="black", weight=3];
33[label="([],[])",fontsize=16,color="green",shape="box"];34[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (Pos (Succ vzz300) > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];34 -> 36[label="",style="solid", color="black", weight=3];
35[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 (Neg (Succ vzz300) > fromInt (Pos Zero))",fontsize=16,color="black",shape="box"];35 -> 37[label="",style="solid", color="black", weight=3];
36[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (compare (Pos (Succ vzz300)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];36 -> 38[label="",style="solid", color="black", weight=3];
37[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 (compare (Neg (Succ vzz300)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];37 -> 39[label="",style="solid", color="black", weight=3];
38[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (primCmpInt (Pos (Succ vzz300)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];38 -> 40[label="",style="solid", color="black", weight=3];
39[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 (primCmpInt (Neg (Succ vzz300)) (fromInt (Pos Zero)) == GT)",fontsize=16,color="black",shape="box"];39 -> 41[label="",style="solid", color="black", weight=3];
40[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (primCmpInt (Pos (Succ vzz300)) (Pos Zero) == GT)",fontsize=16,color="black",shape="box"];40 -> 42[label="",style="solid", color="black", weight=3];
41[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 (primCmpInt (Neg (Succ vzz300)) (Pos Zero) == GT)",fontsize=16,color="black",shape="box"];41 -> 43[label="",style="solid", color="black", weight=3];
42[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (primCmpNat (Succ vzz300) Zero == GT)",fontsize=16,color="black",shape="box"];42 -> 44[label="",style="solid", color="black", weight=3];
43[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 (LT == GT)",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 (GT == GT)",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45[label="genericSplitAt2GenericSplitAt1 (Neg (Succ vzz300)) vzz41 (Neg (Succ vzz300)) vzz40 vzz41 False",fontsize=16,color="black",shape="box"];45 -> 47[label="",style="solid", color="black", weight=3];
46[label="genericSplitAt2GenericSplitAt1 (Pos (Succ vzz300)) vzz41 (Pos (Succ vzz300)) vzz40 vzz41 True",fontsize=16,color="black",shape="box"];46 -> 48[label="",style="solid", color="black", weight=3];
47[label="genericSplitAt0 (Neg (Succ vzz300)) (vzz40 : vzz41)",fontsize=16,color="black",shape="box"];47 -> 49[label="",style="solid", color="black", weight=3];
48[label="(vzz40 : genericSplitAt2Xs' (Pos (Succ vzz300)) vzz41,genericSplitAt2Xs'' (Pos (Succ vzz300)) vzz41)",fontsize=16,color="green",shape="box"];48 -> 50[label="",style="dashed", color="green", weight=3];
48 -> 51[label="",style="dashed", color="green", weight=3];
49[label="error []",fontsize=16,color="black",shape="box"];49 -> 52[label="",style="solid", color="black", weight=3];
50[label="genericSplitAt2Xs' (Pos (Succ vzz300)) vzz41",fontsize=16,color="black",shape="box"];50 -> 53[label="",style="solid", color="black", weight=3];
51[label="genericSplitAt2Xs'' (Pos (Succ vzz300)) vzz41",fontsize=16,color="black",shape="box"];51 -> 54[label="",style="solid", color="black", weight=3];
52[label="error []",fontsize=16,color="red",shape="box"];53 -> 57[label="",style="dashed", color="red", weight=0];
53[label="genericSplitAt2Xs'0 (Pos (Succ vzz300)) vzz41 (genericSplitAt2Vv9 (Pos (Succ vzz300)) vzz41)",fontsize=16,color="magenta"];53 -> 58[label="",style="dashed", color="magenta", weight=3];
54 -> 62[label="",style="dashed", color="red", weight=0];
54[label="genericSplitAt2Xs''0 (Pos (Succ vzz300)) vzz41 (genericSplitAt2Vv9 (Pos (Succ vzz300)) vzz41)",fontsize=16,color="magenta"];54 -> 63[label="",style="dashed", color="magenta", weight=3];
58[label="genericSplitAt2Vv9 (Pos (Succ vzz300)) vzz41",fontsize=16,color="black",shape="triangle"];58 -> 60[label="",style="solid", color="black", weight=3];
57[label="genericSplitAt2Xs'0 (Pos (Succ vzz300)) vzz41 vzz5",fontsize=16,color="burlywood",shape="triangle"];90[label="vzz5/(vzz50,vzz51)",fontsize=10,color="white",style="solid",shape="box"];57 -> 90[label="",style="solid", color="burlywood", weight=9];
90 -> 61[label="",style="solid", color="burlywood", weight=3];
63 -> 58[label="",style="dashed", color="red", weight=0];
63[label="genericSplitAt2Vv9 (Pos (Succ vzz300)) vzz41",fontsize=16,color="magenta"];62[label="genericSplitAt2Xs''0 (Pos (Succ vzz300)) vzz41 vzz6",fontsize=16,color="burlywood",shape="triangle"];92[label="vzz6/(vzz60,vzz61)",fontsize=10,color="white",style="solid",shape="box"];62 -> 92[label="",style="solid", color="burlywood", weight=9];
92 -> 65[label="",style="solid", color="burlywood", weight=3];
60 -> 4[label="",style="dashed", color="red", weight=0];
60[label="genericSplitAt (Pos (Succ vzz300) - fromInt (Pos (Succ Zero))) vzz41",fontsize=16,color="magenta"];60 -> 66[label="",style="dashed", color="magenta", weight=3];
60 -> 67[label="",style="dashed", color="magenta", weight=3];
61[label="genericSplitAt2Xs'0 (Pos (Succ vzz300)) vzz41 (vzz50,vzz51)",fontsize=16,color="black",shape="box"];61 -> 68[label="",style="solid", color="black", weight=3];
65[label="genericSplitAt2Xs''0 (Pos (Succ vzz300)) vzz41 (vzz60,vzz61)",fontsize=16,color="black",shape="box"];65 -> 69[label="",style="solid", color="black", weight=3];
66[label="vzz41",fontsize=16,color="green",shape="box"];67[label="Pos (Succ vzz300) - fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];67 -> 70[label="",style="solid", color="black", weight=3];
68[label="vzz50",fontsize=16,color="green",shape="box"];69[label="vzz61",fontsize=16,color="green",shape="box"];70[label="primMinusInt (Pos (Succ vzz300)) (fromInt (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];70 -> 71[label="",style="solid", color="black", weight=3];
71[label="primMinusInt (Pos (Succ vzz300)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];71 -> 72[label="",style="solid", color="black", weight=3];
72[label="primMinusNat (Succ vzz300) (Succ Zero)",fontsize=16,color="black",shape="box"];72 -> 73[label="",style="solid", color="black", weight=3];
73[label="primMinusNat vzz300 Zero",fontsize=16,color="burlywood",shape="box"];94[label="vzz300/Succ vzz3000",fontsize=10,color="white",style="solid",shape="box"];73 -> 94[label="",style="solid", color="burlywood", weight=9];
94 -> 74[label="",style="solid", color="burlywood", weight=3];
95[label="vzz300/Zero",fontsize=10,color="white",style="solid",shape="box"];73 -> 95[label="",style="solid", color="burlywood", weight=9];
95 -> 75[label="",style="solid", color="burlywood", weight=3];
74[label="primMinusNat (Succ vzz3000) Zero",fontsize=16,color="black",shape="box"];74 -> 76[label="",style="solid", color="black", weight=3];
75[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];75 -> 77[label="",style="solid", color="black", weight=3];
76[label="Pos (Succ vzz3000)",fontsize=16,color="green",shape="box"];77[label="Pos Zero",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ LetRed

                        ↳ HASKELL

                          ↳ NumRed

                            ↳ HASKELL

                              ↳ Narrow

                                ↳ QDP

                                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_genericSplitAt2Vv9(vzz300, vzz41, ba) → new_genericSplitAt(new_primMinusNat(vzz300), vzz41, ba)
new_genericSplitAt(Pos(Succ(vzz300)), :(vzz40, vzz41), ba) → new_genericSplitAt2Vv9(vzz300, vzz41, ba)
new_genericSplitAt(Pos(Succ(vzz300)), :(vzz40, vzz41), ba) → new_genericSplitAt(new_primMinusNat(vzz300), vzz41, ba)

The TRS R consists of the following rules:

new_primMinusNat(Succ(vzz3000)) → Pos(Succ(vzz3000))
new_primMinusNat(Zero) → Pos(Zero)

The set Q consists of the following terms:

new_primMinusNat(Zero)
new_primMinusNat(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_genericSplitAt(Pos(Succ(vzz300)), :(vzz40, vzz41), ba) → new_genericSplitAt2Vv9(vzz300, vzz41, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
new_genericSplitAt(Pos(Succ(vzz300)), :(vzz40, vzz41), ba) → new_genericSplitAt(new_primMinusNat(vzz300), vzz41, ba)
The graph contains the following edges 2 > 2, 3 >= 3
new_genericSplitAt2Vv9(vzz300, vzz41, ba) → new_genericSplitAt(new_primMinusNat(vzz300), vzz41, ba)
The graph contains the following edges 2 >= 2, 3 >= 3

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

genericSplitAt	vvx xs	= genericSplitAt5 vvx xs
genericSplitAt	vw []	= genericSplitAt3 vw []
genericSplitAt	n (x : xs)	= genericSplitAt2 n (x : xs)
genericSplitAt	vz wu	= genericSplitAt0 vz wu

genericSplitAt3	vw []	= ([],[])
genericSplitAt3	vvv vvw	= genericSplitAt2 vvv vvw

genericSplitAt4	True vvx xs	= ([],xs)
genericSplitAt4	vvy vvz vwu	= genericSplitAt3 vvz vwu

genericSplitAt5	vvx xs	= genericSplitAt4 (vvx == 0) vvx xs
genericSplitAt5	vwv vww	= genericSplitAt3 vwv vww

compare2	x y True	= EQ
compare2	x y False	= compare1 x y (x <= y)

compare1	x y True	= LT
compare1	x y False	= compare0 x y otherwise

gcd'2	x vwx	= gcd'1 (vwx == 0) x vwx
gcd'2	vxv vxw	= gcd'0 vxv vxw

gcd2	True vxx vxy	= gcd1 (vxy == 0) vxx vxy
gcd2	vyw vyx vyy	= gcd0 vyx vyy

gcd3	vxx vxy	= gcd2 (vxx == 0) vxx vxy
gcd3	vyz vzu	= gcd0 vyz vzu

genericSplitAt2GenericSplitAt1	vzv vzw n x xs True	= (x : genericSplitAt2Xs' vzv vzw,genericSplitAt2Xs'' vzv vzw)
genericSplitAt2GenericSplitAt1	vzv vzw n x xs False	= genericSplitAt0 n (x : xs)

reduce2Reduce1	vzx vzy x y True	= error []
reduce2Reduce1	vzx vzy x y False	= reduce2Reduce0 vzx vzy x y otherwise

gcd0Gcd'2	x vwx	= gcd0Gcd'1 (vwx == 0) x vwx
gcd0Gcd'2	vxv vxw	= gcd0Gcd'0 vxv vxw

gcd0Gcd'1	True x vwx	= x
gcd0Gcd'1	vwy vwz vxu	= gcd0Gcd'0 vwz vxu